(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UF)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun v11 () Bool)
(declare-fun v12 () Bool)
(declare-fun v13 () Bool)
(declare-fun v14 () Bool)
(declare-fun v15 () Bool)
(declare-fun v16 () Bool)
(declare-fun v17 () Bool)
(declare-fun v18 () Bool)
(declare-fun v19 () Bool)
(declare-fun v20 () Bool)
(declare-fun v21 () Bool)
(declare-fun v22 () Bool)
(declare-fun v23 () Bool)
(declare-fun v24 () Bool)
(declare-fun v25 () Bool)
(declare-fun v26 () Bool)
(declare-fun v27 () Bool)
(declare-fun v28 () Bool)
(declare-fun v29 () Bool)
(declare-fun v30 () Bool)
(declare-fun v31 () Bool)
(declare-fun v32 () Bool)
(declare-fun v33 () Bool)
(declare-fun v34 () Bool)
(declare-fun v35 () Bool)
(declare-fun v36 () Bool)
(declare-fun v37 () Bool)
(declare-fun v38 () Bool)
(declare-fun v39 () Bool)
(declare-fun v40 () Bool)
(declare-fun v41 () Bool)
(declare-fun v42 () Bool)
(declare-fun v43 () Bool)
(declare-fun v44 () Bool)
(declare-fun v45 () Bool)
(declare-fun v46 () Bool)
(declare-fun v47 () Bool)
(declare-fun v48 () Bool)
(declare-fun v49 () Bool)
(declare-fun v50 () Bool)
(declare-fun v51 () Bool)
(declare-fun v52 () Bool)
(declare-fun v53 () Bool)
(declare-fun v54 () Bool)
(declare-fun v55 () Bool)
(declare-fun v56 () Bool)
(declare-fun v57 () Bool)
(declare-fun v58 () Bool)
(declare-fun v59 () Bool)
(declare-fun v60 () Bool)
(declare-fun v61 () Bool)
(declare-fun v62 () Bool)
(declare-fun v63 () Bool)
(declare-fun v64 () Bool)
(declare-fun v65 () Bool)
(declare-fun v66 () Bool)
(declare-fun v67 () Bool)
(declare-fun v68 () Bool)
(declare-fun v69 () Bool)
(declare-fun v70 () Bool)
(declare-fun v71 () Bool)
(declare-fun v72 () Bool)
(declare-fun v73 () Bool)
(declare-fun v74 () Bool)
(declare-fun v75 () Bool)
(declare-fun v76 () Bool)
(declare-fun v77 () Bool)
(declare-fun v78 () Bool)
(declare-fun v79 () Bool)
(declare-fun v80 () Bool)
(declare-fun v81 () Bool)
(declare-fun v82 () Bool)
(declare-fun v83 () Bool)
(declare-fun v84 () Bool)
(assert (let ((e85 
(and
 (or (not v24) (not v70) v58)
 (or (not v27) v71 (not v74))
 (or (not v19) (not v58) v25)
 (or (not v28) v68 (not v19))
 (or (not v52) v9 v54)
 (or v79 v7 v82)
 (or (not v6) v16 (not v33))
 (or (not v54) (not v81) (not v41))
 (or v70 (not v43) (not v73))
 (or (not v37) v30 v11)
 (or (not v81) (not v45) v6)
 (or v24 v12 v40)
 (or (not v39) v3 v63)
 (or (not v84) v53 (not v7))
 (or (not v25) (not v27) (not v48))
 (or (not v70) v69 (not v79))
 (or (not v50) (not v71) (not v49))
 (or (not v61) v16 v11)
 (or (not v54) v22 (not v62))
 (or (not v31) v57 (not v53))
 (or (not v58) v60 v10)
 (or (not v58) v77 (not v51))
 (or (not v55) (not v42) (not v8))
 (or v61 (not v6) v56)
 (or v59 v50 v33)
 (or v51 v18 (not v41))
 (or v37 (not v16) v69)
 (or v1 v48 (not v71))
 (or v81 v11 v43)
 (or (not v10) (not v23) v79)
 (or (not v39) (not v42) v67)
 (or v63 v17 v72)
 (or (not v75) (not v74) v40)
 (or v68 (not v45) (not v35))
 (or (not v21) v75 (not v54))
 (or v17 (not v44) (not v43))
 (or v48 v83 (not v29))
 (or v75 (not v43) (not v20))
 (or v48 (not v23) v46)
 (or (not v6) (not v63) v46)
 (or v16 (not v42) v51)
 (or (not v81) (not v65) (not v44))
 (or (not v81) (not v43) v37)
 (or v25 v72 v37)
 (or v61 (not v47) v45)
 (or v2 (not v28) (not v59))
 (or v25 (not v33) v10)
 (or v1 v64 (not v60))
 (or (not v66) (not v74) v13)
 (or (not v38) (not v50) v25)
 (or (not v71) v78 v41)
 (or (not v64) (not v45) (not v82))
 (or (not v73) v41 (not v27))
 (or (not v42) v32 (not v50))
 (or v15 v29 (not v10))
 (or v11 (not v9) (not v66))
 (or v78 (not v39) v68)
 (or v11 (not v13) v81)
 (or (not v36) (not v18) (not v12))
 (or (not v36) (not v62) v12)
 (or (not v28) v7 (not v72))
 (or v13 v79 v36)
 (or v40 v55 (not v14))
 (or (not v82) (not v56) v69)
 (or (not v32) v28 (not v59))
 (or v50 v66 v53)
 (or v67 v62 (not v67))
 (or v2 (not v11) v2)
 (or (not v34) v78 v24)
 (or (not v11) v79 v19)
 (or (not v4) (not v60) v64)
 (or v79 (not v37) (not v10))
 (or (not v82) v58 v80)
 (or (not v8) (not v69) v13)
 (or (not v62) (not v26) v74)
 (or (not v55) v47 (not v35))
 (or (not v7) v69 (not v39))
 (or (not v22) (not v72) (not v40))
 (or v40 (not v8) (not v53))
 (or (not v31) v36 (not v42))
 (or (not v5) v10 v17)
 (or (not v44) (not v7) (not v33))
 (or (not v29) v4 (not v78))
 (or v51 v60 (not v1))
 (or (not v34) (not v21) (not v14))
 (or v28 (not v16) (not v70))
 (or v55 (not v18) v50)
 (or (not v36) (not v1) v78)
 (or v19 (not v63) (not v77))
 (or (not v20) v39 (not v0))
 (or (not v78) v58 (not v19))
 (or v80 (not v83) (not v35))
 (or v15 v16 v15)
 (or v24 v54 v68)
 (or v10 (not v84) v32)
 (or v10 v15 v53)
 (or v22 (not v64) v80)
 (or (not v24) v34 (not v20))
 (or (not v7) (not v41) v74)
 (or (not v29) v15 (not v20))
 (or v30 (not v40) v51)
 (or v66 v32 (not v37))
 (or v4 (not v32) v26)
 (or v11 (not v53) v76)
 (or v41 (not v10) (not v21))
 (or v24 v66 (not v14))
 (or (not v72) v61 (not v38))
 (or v18 v9 (not v50))
 (or v74 (not v43) v18)
 (or (not v13) v80 (not v68))
 (or (not v71) (not v21) (not v8))
 (or v56 v54 v76)
 (or (not v61) (not v1) (not v50))
 (or v62 v68 v11)
 (or v5 v53 (not v23))
 (or (not v49) v82 (not v71))
 (or (not v70) v27 v47)
 (or v7 (not v47) (not v53))
 (or v46 (not v70) (not v60))
 (or (not v25) v69 (not v73))
 (or (not v58) (not v57) v60)
 (or v1 (not v81) (not v7))
 (or (not v43) (not v66) v77)
 (or (not v73) v60 (not v11))
 (or (not v51) v26 v81)
 (or v70 v37 v17)
 (or (not v75) (not v75) (not v80))
 (or (not v6) v39 v21)
 (or (not v77) v53 v23)
 (or (not v27) v32 v10)
 (or (not v9) v56 v47)
 (or (not v27) v21 (not v47))
 (or v9 (not v75) v31)
 (or (not v74) (not v62) v44)
 (or (not v67) (not v78) v47)
 (or (not v18) (not v58) (not v14))
 (or (not v63) v70 v14)
 (or v11 v51 v66)
 (or (not v66) v23 (not v3))
 (or v82 (not v63) (not v32))
 (or (not v40) (not v4) v29)
 (or (not v29) (not v27) (not v47))
 (or (not v72) v19 (not v31))
 (or v47 v65 v15)
 (or v17 (not v62) v64)
 (or v78 (not v67) (not v66))
 (or (not v67) v18 v19)
 (or (not v13) v57 v57)
 (or (not v46) (not v75) v38)
 (or (not v5) v54 v37)
 (or (not v82) v84 v79)
 (or (not v51) v41 (not v4))
 (or v1 v59 v33)
 (or (not v53) v79 v15)
 (or (not v25) (not v45) v76)
 (or v15 (not v51) v4)
 (or (not v26) (not v19) (not v44))
 (or (not v0) (not v7) v62)
 (or (not v5) v77 (not v79))
 (or (not v3) (not v14) (not v4))
 (or (not v74) v39 (not v47))
 (or (not v32) v6 v52)
 (or v11 v54 (not v20))
 (or (not v44) v25 v28)
 (or (not v78) (not v69) v44)
 (or (not v24) (not v64) v17)
 (or v74 v69 (not v44))
 (or (not v24) (not v63) v71)
 (or (not v41) (not v31) (not v19))
 (or v58 v24 (not v45))
 (or (not v28) (not v30) (not v11))
 (or (not v63) (not v50) (not v81))
 (or (not v51) (not v74) v46)
 (or (not v5) (not v27) v2)
 (or v72 (not v12) v22)
 (or (not v49) v71 v25)
 (or (not v24) v64 v1)
 (or (not v63) (not v52) v70)
 (or (not v70) (not v5) v51)
 (or (not v66) (not v4) v82)
 (or v35 v59 (not v25))
 (or v60 v12 v17)
 (or v36 v12 (not v35))
 (or v19 v63 (not v81))
 (or v80 v50 (not v40))
 (or v48 v45 (not v66))
 (or (not v62) (not v28) (not v2))
 (or v67 v50 (not v7))
 (or (not v74) (not v32) (not v25))
 (or v57 (not v17) v68)
 (or v11 v25 v50)
 (or (not v1) v49 (not v20))
 (or v35 (not v26) v72)
 (or v4 v69 v40)
 (or v66 v67 v45)
 (or (not v6) v72 v21)
 (or v52 (not v14) v73)
 (or (not v30) v46 (not v6))
 (or (not v73) (not v39) v20)
 (or (not v40) v39 v68)
 (or (not v83) (not v67) v31)
 (or (not v54) (not v15) v72)
 (or (not v29) (not v64) v7)
 (or (not v21) v49 v8)
 (or (not v5) v59 (not v15))
 (or (not v19) (not v9) v15)
 (or v33 (not v22) (not v64))
 (or (not v34) (not v4) v57)
 (or v9 (not v66) (not v64))
 (or v75 v38 v80)
 (or v24 v51 v26)
 (or v42 v25 (not v7))
 (or v56 v25 (not v33))
 (or (not v68) (not v12) (not v50))
 (or v17 v29 (not v74))
 (or v40 v72 (not v80))
 (or v39 (not v25) v56)
 (or v23 (not v82) v1)
 (or v54 v78 (not v40))
 (or v45 v58 v13)
 (or v24 v41 v24)
 (or (not v39) (not v33) v30)
 (or v44 (not v84) v38)
 (or v50 v79 v10)
 (or v47 (not v8) v36)
 (or v40 v65 v76)
 (or v70 v70 (not v16))
 (or (not v55) (not v3) (not v48))
 (or (not v33) (not v11) v18)
 (or v0 v68 (not v23))
 (or v26 v4 (not v0))
 (or v58 v16 v55)
 (or v63 (not v43) v24)
 (or v37 (not v11) v29)
 (or (not v16) (not v40) v19)
 (or (not v17) (not v61) (not v29))
 (or v17 v2 (not v76))
 (or v2 v60 (not v71))
 (or v79 (not v83) (not v32))
 (or (not v15) (not v58) v76)
 (or (not v12) (not v4) v6)
 (or v3 (not v70) v78)
 (or v2 v67 (not v52))
 (or v32 v52 v6)
 (or v12 (not v2) v2)
 (or (not v76) (not v24) (not v9))
 (or (not v75) (not v10) v61)
 (or v19 (not v15) v73)
 (or v0 (not v64) (not v59))
 (or v55 v53 (not v75))
 (or (not v28) v58 v61)
 (or v54 (not v16) (not v63))
 (or (not v48) (not v49) (not v45))
 (or v62 (not v55) (not v36))
 (or (not v58) (not v30) v13)
 (or (not v8) (not v70) (not v62))
 (or v78 (not v78) v34)
 (or (not v62) (not v72) (not v25))
 (or (not v35) v54 (not v28))
 (or (not v78) (not v5) v20)
 (or (not v47) v16 (not v50))
 (or (not v58) v3 (not v47))
 (or v43 v29 (not v40))
 (or (not v57) (not v4) (not v24))
 (or (not v54) (not v0) (not v59))
 (or (not v54) v3 v17)
 (or (not v67) (not v52) v31)
 (or (not v47) v65 v56)
 (or v43 v52 (not v27))
 (or v71 v71 v52)
 (or v70 (not v80) v52)
 (or (not v4) v70 (not v27))
 (or v82 (not v84) (not v15))
 (or (not v26) v44 v74)
 (or (not v58) (not v31) (not v34))
 (or v29 (not v42) v14)
 (or (not v43) (not v41) (not v7))
 (or v25 v39 (not v53))
 (or (not v5) v56 v11)
 (or v42 (not v54) v55)
 (or v36 v81 (not v3))
 (or v32 v84 (not v4))
 (or (not v36) (not v33) v52)
 (or (not v43) (not v66) v45)
 (or (not v46) v73 (not v72))
 (or v79 (not v65) (not v53))
 (or (not v56) (not v35) (not v28))
 (or (not v52) (not v35) v74)
 (or v79 (not v6) (not v8))
 (or (not v67) v27 v3)
 (or v20 v36 (not v52))
 (or v23 v36 v36)
 (or v52 (not v39) (not v22))
 (or (not v58) v55 v62)
 (or v22 v32 (not v20))
 (or v7 (not v24) (not v35))
 (or v21 v71 (not v37))
 (or v24 v61 (not v28))
 (or v35 v33 (not v13))
 (or (not v71) v16 v34)
 (or (not v22) (not v69) v75)
 (or (not v41) v62 (not v38))
 (or (not v70) (not v27) v8)
 (or v14 v47 v4)
 (or (not v35) v28 v68)
 (or v44 (not v51) v33)
 (or (not v26) (not v36) v20)
 (or v78 v46 (not v66))
 (or (not v64) v61 (not v84))
 (or v61 v20 v57)
 (or (not v44) v37 (not v46))
 (or (not v78) v13 (not v20))
 (or v80 v6 (not v76))
 (or (not v23) v47 (not v75))
 (or (not v54) v23 (not v45))
 (or (not v79) (not v41) (not v18))
 (or (not v14) v41 v6)
 (or (not v29) v81 (not v40))
 (or v73 (not v34) (not v11))
 (or (not v80) (not v77) v83)
 (or v84 (not v55) (not v24))
 (or (not v53) (not v35) (not v37))
 (or v35 v69 (not v64))
 (or (not v84) v20 (not v70))
 (or v64 v33 v1)
 (or (not v30) v61 (not v77))
 (or (not v39) (not v79) (not v54))
 (or (not v31) v50 (not v33))
 (or v71 v17 v82)
 (or (not v47) (not v62) v31)
 (or v75 v61 (not v24))
 (or (not v59) (not v13) (not v6))
 (or (not v70) (not v18) v80)
 (or (not v82) (not v22) (not v19))
 (or v75 (not v14) v60)
 (or (not v43) (not v31) (not v13))
 (or (not v15) v36 v70)
 (or v73 v38 (not v4))
 (or (not v20) v77 v71)
 (or (not v24) v50 v21)
 (or v10 v84 (not v3))
 (or v43 v22 (not v66))
 (or (not v63) v55 v33)
 (or v5 v22 (not v71))
 (or v74 (not v22) (not v60))
 (or v24 (not v42) (not v43))
 (or v34 (not v36) (not v54))
 (or (not v8) (not v2) v69)
 (or v9 (not v13) (not v44))
 (or v14 v83 v6)
 (or v76 (not v17) v35)
 (or v70 (not v8) (not v30))
 (or (not v36) (not v25) v32)
 (or v75 (not v63) v69)
 (or v79 (not v17) v34)
 (or v65 v54 (not v84))
 (or v61 (not v78) (not v5))
 (or v57 (not v84) (not v62))
 (or (not v46) v80 (not v45))
 (or (not v40) (not v68) v80)
 (or (not v80) v20 (not v20))
 (or (not v28) v3 v49)
 (or v54 (not v10) v12)
 (or (not v82) v19 v52)
 (or v59 v23 v56)
 (or v39 (not v80) v46)
 (or (not v23) (not v32) (not v46))
 (or (not v14) v57 v42)
 (or v14 v17 (not v82))
 (or (not v77) v52 v25)
 (or v33 (not v43) (not v72))
 (or v63 (not v51) v7)
 (or (not v71) (not v23) v7)
 (or v55 v39 v40)
 (or (not v69) v48 (not v32))
 (or (not v4) (not v69) (not v10))
 (or v64 (not v45) (not v75))
 (or (not v6) v68 (not v50))
 (or v32 (not v56) v34)
 (or (not v2) (not v0) (not v73))
 (or (not v24) v56 (not v39))
 (or (not v3) v10 (not v19))
 (or (not v12) v56 (not v43))
 (or v58 (not v13) v34)
 (or v29 v4 (not v83))
 (or (not v68) (not v55) (not v56))
 (or v71 v6 (not v35))
 (or v8 v27 (not v76))
 (or v38 (not v75) (not v46))
 (or v16 (not v76) (not v78))
 (or (not v26) v29 v79)
 (or v0 (not v75) v68)
 (or (not v0) (not v14) v80)
 (or v13 (not v44) v18)
 (or v13 (not v78) (not v65))
 (or (not v40) v7 v1)
 (or v79 (not v60) v81)
 (or v64 v31 v56)
 (or v59 (not v77) (not v67))
 (or v30 (not v80) v18)
 (or (not v33) v15 v12)
 (or (not v45) v52 v57)
 (or (not v80) (not v70) v11)
 (or (not v5) (not v16) (not v41))
 (or v73 (not v10) (not v9))
 (or v10 v58 (not v30))
 (or v61 v66 v40)
 (or (not v18) (not v33) v64)
 (or (not v78) (not v66) (not v4))
 (or (not v74) v18 (not v6))
 (or (not v31) (not v21) (not v3))
 (or (not v76) (not v2) v75)
 (or v18 v19 (not v75))
 (or v72 v80 v33)
 (or v22 (not v64) (not v49))
 (or (not v5) (not v70) (not v46))
 (or v33 v73 v17)
 (or (not v6) (not v29) v0)
 (or (not v68) v17 v44)
 (or (not v5) v27 (not v80))
 (or (not v62) v78 (not v12))
 (or (not v75) v15 (not v16))
 (or (not v58) v11 v1)
 (or v64 (not v75) v16)
 (or (not v25) (not v82) (not v11))
 (or (not v43) v74 (not v9))
 (or v71 (not v79) v62)
 (or v24 v0 (not v61))
 (or (not v81) v28 (not v59))
 (or v47 (not v36) (not v38))
 (or v19 v77 (not v34))
 (or v40 v37 v21)
 (or (not v47) v54 (not v32))
 (or v57 v1 (not v42))
 (or (not v73) v46 v24)
 (or v13 (not v61) v67)
 (or (not v29) v4 (not v14))
 (or (not v56) (not v58) (not v82))
 (or v39 (not v64) v73)
 (or (not v44) v17 v29)
 (or (not v29) v77 v4)
 (or (not v19) (not v7) (not v27))
 (or v45 v80 (not v66))
 (or v19 v11 v28)
 (or v65 v26 v57)
 (or (not v1) v5 (not v2))
 (or v1 (not v56) (not v69))
 (or v13 v84 (not v54))
 (or (not v74) (not v16) v3)
 (or v48 (not v43) (not v70))
 (or (not v59) v13 (not v67))
 (or v39 (not v13) v32)
 (or v17 v57 v76)
 (or (not v70) (not v25) v4)
 (or v24 v82 (not v39))
 (or (not v47) v18 v56)
 (or v29 (not v68) v17)
 (or (not v1) (not v35) v19)
 (or v15 (not v38) v31)
 (or (not v29) (not v20) v0)
 (or v20 v65 (not v67))
 (or (not v10) v82 (not v52))
 (or (not v50) v18 v62)
 (or (not v78) (not v58) v9)
 (or (not v12) (not v3) v1)
 (or (not v44) (not v84) v30)
 (or (not v27) (not v74) (not v8))
 (or v18 v2 v70)
 (or (not v5) (not v51) (not v20))
 (or v38 (not v38) v40)
 (or v8 (not v67) (not v26))
 (or (not v73) v24 (not v15))
 (or (not v78) v56 (not v35))
 (or v9 (not v10) v46)
 (or (not v48) (not v37) v51)
 (or v75 v55 v72)
 (or (not v27) v61 v13)
 (or v48 v18 (not v23))
 (or (not v53) v18 v71)
 (or (not v83) v10 (not v24))
 (or v16 (not v67) v77)
 (or (not v34) (not v20) v52)
 (or (not v71) (not v22) (not v51))
 (or v29 (not v37) v83)
 (or v11 (not v74) v42)
 (or v65 (not v20) (not v41))
 (or (not v72) v4 v65)
 (or v2 v69 v28)
 (or (not v40) (not v29) v23)
 (or (not v1) (not v20) (not v52))
 (or (not v25) (not v14) (not v33))
 (or v38 v74 v14)
 (or v36 v42 v59)
 (or (not v73) (not v71) (not v33))
 (or v28 v60 v84)
 (or (not v66) v68 v51)
 (or v72 (not v62) v64)
 (or v42 (not v53) v79)
 (or v2 (not v36) (not v36))
 (or v11 (not v29) (not v84))
 (or v61 (not v82) (not v76))
 (or (not v49) v42 v69)
 (or v14 (not v78) v26)
 (or v22 (not v9) (not v40))
 (or (not v11) v81 v15)
 (or (not v37) v37 v13)
 (or (not v55) v18 v16)
 (or (not v5) (not v77) v39)
 (or (not v62) (not v48) v40)
 (or v10 (not v16) v5)
 (or (not v66) (not v16) v65)
 (or (not v52) v9 (not v78))
 (or (not v64) v38 (not v67))
 (or v79 (not v70) (not v9))
 (or v27 v29 (not v28))
 (or (not v76) (not v66) (not v20))
 (or (not v56) (not v73) v35)
 (or (not v9) v14 (not v3))
 (or (not v10) (not v33) v25)
 (or v63 (not v18) (not v40))
 (or v45 (not v41) (not v80))
 (or v82 (not v20) v54)
 (or (not v37) (not v34) v74)
 (or (not v12) v76 v57)
 (or (not v16) v66 (not v62))
 (or v61 (not v21) v42)
 (or (not v36) v51 (not v49))
 (or v84 (not v33) v36)
 (or (not v74) v21 v14)
 (or v62 v19 v70)
 (or v26 v78 v31)
 (or (not v28) (not v20) v39)
 (or (not v5) (not v27) (not v75))
 (or v37 v35 (not v60))
 (or v35 v6 (not v11))
 (or v80 v50 v29)
 (or (not v45) (not v36) v2)
 (or (not v80) (not v47) v3)
 (or v79 (not v63) (not v82))
 (or v4 v30 v45)
 (or v62 (not v65) v81)
 (or (not v22) v58 v3)
 (or (not v15) (not v42) v74)
 (or (not v61) v42 (not v69))
 (or (not v62) (not v58) v6)
 (or v6 (not v41) (not v5))
 (or v1 (not v37) (not v46))
 (or v63 v9 v68)
 (or v77 (not v33) (not v76))
 (or (not v61) v42 v14)
 (or v5 (not v83) (not v31))
 (or v17 v75 v47)
 (or v23 (not v37) v32)
 (or v24 (not v3) (not v16))
 (or v67 (not v66) v9)
 (or v77 (not v25) v5)
 (or v11 (not v3) v71)
 (or v39 (not v45) (not v53))
 (or v55 (not v46) v71)
 (or (not v25) (not v45) (not v6))
 (or (not v48) (not v68) v84)
 (or (not v62) (not v78) (not v59))
 (or v62 (not v28) v70)
 (or (not v1) (not v66) (not v84))
 (or (not v38) (not v57) v47)
 (or v3 v35 v84)
 (or (not v43) (not v57) v27)
 (or v67 (not v34) (not v67))
 (or v56 v8 v74)
 (or (not v77) (not v65) (not v7))
 (or (not v15) (not v45) v25)
 (or (not v80) (not v38) (not v21))
 (or v15 v55 v17)
 (or (not v63) (not v41) (not v39))
 (or v34 v21 (not v69))
 (or v80 v39 v2)
 (or (not v6) v53 v25)
 (or (not v4) (not v77) (not v20))
 (or (not v13) v28 (not v43))
 (or (not v45) (not v70) v33)
 (or v38 (not v74) v75)
 (or v52 (not v69) (not v12))
 (or (not v32) (not v69) v48)
 (or (not v21) v12 v2)
 (or v18 v58 (not v28))
 (or (not v44) v21 v16)
 (or v14 v18 v30)
 (or v25 (not v30) v28)
 (or (not v76) (not v83) v17)
 (or (not v32) (not v71) v10)
 (or (not v78) v49 v53)
 (or (not v47) (not v76) v16)
 (or (not v2) v18 (not v34))
 (or v16 v58 (not v57))
 (or (not v1) v73 v1)
 (or (not v18) v21 v25)
 (or (not v64) (not v1) v61)
 (or v5 v13 v73)
 (or (not v0) v55 v39)
 (or (not v14) v18 (not v80))
 (or v69 (not v9) (not v65))
 (or v66 (not v67) (not v62))
 (or (not v41) (not v52) v18)
 (or v57 v46 v29)
 (or v14 v60 (not v58))
 (or (not v13) v49 v28)
 (or (not v11) v59 (not v53))
 (or (not v17) (not v28) v11)
 (or v50 (not v83) v73)
 (or v38 (not v14) (not v76))
 (or v50 v82 (not v5))
 (or v3 v77 (not v45))
 (or (not v57) v83 v62)
 (or v48 v56 (not v13))
 (or v50 v27 (not v1))
 (or (not v67) v59 (not v53))
 (or (not v70) (not v25) v1)
 (or v80 v54 (not v45))
 (or (not v48) v24 v79)
 (or v40 v6 (not v11))
 (or v26 v20 (not v16))
 (or (not v26) (not v50) v17)
 (or (not v42) (not v51) v65)
 (or (not v45) (not v5) v67)
 (or v41 (not v61) (not v45))
 (or (not v29) v57 (not v71))
 (or (not v61) (not v24) v61)
 (or v63 v2 (not v21))
 (or v13 (not v68) v72)
 (or (not v83) v84 (not v44))
 (or (not v23) v62 (not v74))
 (or (not v47) v28 (not v21))
 (or v13 (not v13) v21)
 (or v59 v38 v64)
 (or (not v24) v72 v83)
 (or v78 (not v12) (not v67))
 (or (not v5) (not v45) (not v12))
 (or v29 v48 v48)
 (or v68 v1 v58)
 (or (not v71) (not v36) (not v28))
 (or (not v25) (not v17) v4)
 (or v59 v7 (not v53))
 (or (not v50) v20 (not v76))
 (or (not v40) v25 v57)
 (or v79 v53 (not v33))
 (or (not v2) v18 v32)
 (or v64 (not v50) (not v2))
 (or (not v79) v22 (not v36))
 (or v10 (not v15) v70)
 (or v35 (not v57) v69)
 (or (not v12) (not v5) (not v63))
 (or v43 v15 (not v76))
 (or (not v18) v63 v61)
 (or v49 v36 (not v36))
 (or v42 v2 v82)
 (or (not v37) v71 (not v69))
 (or v12 v55 v0)
 (or (not v44) (not v45) (not v37))
 (or v50 v57 (not v51))
 (or v7 v48 v33)
 (or (not v22) v82 v8)
 (or v71 v5 (not v10))
 (or (not v24) v56 v17)
 (or (not v16) (not v9) v45)
 (or v24 (not v42) v83)
 (or (not v75) v8 v45)
 (or v55 (not v53) v38)
 (or v82 v32 (not v67))
 (or (not v29) (not v21) v72)
 (or v24 v4 v32)
 (or (not v8) v46 (not v78))
 (or (not v60) v15 v1)
 (or (not v49) (not v54) v32)
 (or v79 v77 (not v41))
 (or (not v37) v58 v20)
 (or v30 (not v61) v16)
 (or v61 v23 (not v29))
 (or v42 v30 (not v79))
 (or (not v23) (not v6) v5)
 (or v44 (not v40) v70)
 (or (not v52) (not v10) (not v39))
 (or (not v21) (not v77) v49)
 (or (not v2) (not v14) (not v8))
 (or (not v55) v64 (not v18))
 (or v33 v7 (not v40))
 (or (not v66) (not v80) (not v11))
 (or (not v28) v82 (not v38))
 (or v81 v72 v48)
 (or v25 (not v83) (not v17))
 (or (not v30) (not v40) (not v3))
 (or (not v78) v44 (not v14))
 (or v2 (not v5) v77)
 (or v14 v9 v24)
 (or (not v51) (not v69) (not v57))
 (or v63 v28 v31)
 (or (not v84) (not v75) (not v34))
 (or v8 (not v5) (not v30))
 (or (not v69) v80 v11)
 (or (not v58) v40 v36)
 (or (not v69) v8 v20)
 (or v31 v19 (not v70))
 (or v28 v66 (not v12))
 (or (not v64) v23 v44)
 (or v1 (not v23) (not v54))
 (or (not v37) v1 v77)
 (or (not v59) v71 v54)
 (or (not v29) v1 v23)
 (or v6 (not v75) v66)
 (or (not v52) (not v19) v51)
 (or v15 (not v47) (not v54))
 (or v35 v49 (not v12))
 (or v83 v55 (not v81))
 (or v55 (not v22) (not v82))
 (or (not v36) (not v26) v25)
 (or v45 v73 (not v80))
 (or v80 (not v48) (not v26))
 (or (not v19) v60 (not v47))
 (or v78 (not v70) v15)
 (or v47 v60 (not v53))
 (or (not v5) v4 v47)
 (or v36 v68 v2)
 (or (not v78) (not v28) (not v82))
 (or v49 (not v62) (not v68))
 (or v27 (not v52) v34)
 (or v75 v19 v63)
 (or (not v61) v73 (not v65))
 (or (not v10) v64 (not v68))
 (or v30 (not v54) v2)
 (or (not v45) (not v68) v74)
 (or v77 (not v71) v25)
 (or v3 (not v38) v28)
 (or v27 v8 v80)
 (or (not v2) v18 (not v72))
 (or v69 v23 (not v53))
 (or (not v76) (not v74) v82)
 (or (not v57) v47 v80)
 (or v27 v69 v78)
 (or v43 (not v43) (not v63))
 (or v32 (not v3) v13)
 (or (not v36) (not v46) (not v12))
 (or v10 (not v15) v72)
 (or (not v5) (not v62) (not v64))
 (or v70 v61 v51)
 (or v9 (not v82) v30)
 (or v49 (not v81) v44)
 (or v47 (not v30) (not v68))
 (or v15 (not v75) (not v3))
 (or v19 (not v34) (not v53))
 (or v18 v81 (not v76))
 (or v2 v35 (not v53))
 (or (not v0) (not v48) (not v2))
 (or v62 (not v55) (not v61))
 (or (not v9) v45 v41)
 (or (not v69) v75 (not v67))
 (or v65 v81 (not v6))
 (or (not v6) v59 v54)
 (or v8 (not v62) (not v40))
 (or v21 (not v16) (not v58))
 (or (not v47) (not v27) v61)
 (or (not v31) (not v10) (not v30))
 (or v24 (not v44) v41)
 (or v45 (not v68) v21)
 (or v42 v45 (not v19))
 (or (not v84) (not v77) v26)
 (or v16 (not v34) (not v74))
 (or v4 v65 v2)
 (or v52 v35 v78)
 (or (not v36) (not v75) v58)
 (or (not v9) v84 v32)
 (or v74 (not v25) (not v66))
 (or (not v57) (not v80) (not v15))
 (or (not v47) (not v73) (not v18))
 (or v75 v18 (not v12))
 (or (not v35) (not v31) v41)
 (or (not v29) (not v14) (not v57))
 (or (not v15) v43 (not v53))
 (or (not v75) (not v81) (not v64))
 (or (not v80) (not v10) v6)
 (or (not v59) (not v18) v74)
 (or (not v40) (not v14) (not v2))
 (or v39 v44 (not v58))
 (or (not v44) (not v3) (not v16))
 (or (not v31) v58 v11)
 (or (not v51) v70 (not v82))
 (or v69 v16 v53)
 (or (not v45) (not v11) v0)
 (or v16 (not v73) v36)
 (or v11 (not v47) v46)
 (or v68 v70 (not v19))
 (or (not v9) v68 v34)
 (or v10 v8 (not v16))
 (or v30 (not v30) v51)
 (or v63 v35 (not v23))
 (or (not v27) (not v3) v0)
 (or (not v27) v24 (not v21))
 (or v82 (not v71) v29)
 (or v12 (not v62) (not v71))
 (or v11 v1 (not v41))
 (or (not v38) (not v50) v43)
 (or (not v74) (not v27) v47)
 (or v67 (not v51) (not v32))
 (or v51 (not v1) v67)
 (or (not v44) v84 (not v39))
 (or v59 v70 v48)
 (or (not v67) v13 (not v79))
 (or v47 v6 (not v76))
 (or (not v59) v66 (not v47))
 (or (not v81) v14 (not v29))
 (or v11 (not v40) (not v72))
 (or (not v65) (not v55) v74)
 (or (not v29) (not v65) (not v46))
 (or (not v48) v39 v58)
 (or v83 (not v68) v2)
 (or (not v1) (not v27) (not v63))
 (or v12 (not v52) (not v54))
 (or (not v33) v76 (not v12))
 (or (not v49) (not v33) v78)
 (or (not v22) v37 (not v55))
 (or v50 v16 (not v25))
 (or (not v65) (not v35) v15)
 (or v77 (not v30) v38)
 (or (not v81) (not v56) (not v80))
 (or v43 (not v35) (not v40))
 (or (not v31) (not v81) (not v20))
 (or v38 (not v20) (not v83))
 (or (not v82) v66 v73)
 (or (not v45) v79 v77)
 (or v1 (not v83) v51)
 (or (not v24) (not v57) (not v26))
 (or (not v64) (not v46) v32)
 (or (not v65) v69 v0)
 (or (not v79) (not v57) (not v11))
 (or v8 (not v25) (not v78))
 (or (not v45) v78 v75)
 (or v71 (not v46) v41)
 (or (not v25) v70 v68)
 (or (not v80) (not v21) v77)
 (or v10 (not v46) v66)
 (or (not v11) v59 v20)
 (or (not v48) (not v42) v45)
 (or v65 v16 v41)
 (or v74 (not v21) (not v28))
 (or (not v49) v29 (not v3))
 (or v32 v80 v82)
 (or v32 (not v45) v49)
 (or (not v43) v27 v84)
 (or v33 (not v26) v3)
 (or v21 (not v68) v74)
 (or v48 (not v24) (not v78))
 (or (not v0) v84 v77)
 (or v14 v65 (not v46))
 (or v64 v55 v4)
 (or (not v49) v79 v11)
 (or (not v64) v52 (not v53))
 (or (not v43) v68 v40)
 (or v80 (not v34) v61)
 (or (not v70) v46 v42)
 (or v27 v39 (not v42))
 (or v4 (not v70) (not v66))
 (or v18 (not v0) (not v81))
 (or v28 v75 v46)
 (or (not v19) v17 v4)
 (or v1 v49 v73)
 (or v7 (not v83) v51)
 (or v82 v18 (not v3))
 (or v52 v22 (not v18))
 (or (not v48) (not v0) v37)
 (or v8 (not v68) (not v30))
 (or (not v3) (not v29) v23)
 (or (not v3) v69 v66)
 (or v72 v15 (not v65))
 (or v24 v22 v23)
 (or v30 (not v7) (not v67))
 (or (not v22) v59 v70)
 (or v54 (not v3) v66)
 (or (not v22) v51 (not v54))
 (or (not v35) v78 v47)
 (or v34 (not v45) (not v56))
 (or v82 (not v4) (not v47))
 (or v3 (not v1) (not v16))
 (or (not v82) v74 v75)
 (or v55 v22 v33)
 (or v75 v32 v65)
 (or v32 (not v17) (not v22))
 (or (not v45) (not v81) (not v0))
 (or (not v70) (not v48) v58)
 (or (not v36) (not v29) v26)
 (or v73 (not v4) v15)
 (or v70 v9 v49)
 (or v35 v77 v17)
 (or v56 (not v66) v46)
 (or v30 (not v33) (not v18))
 (or v61 (not v18) v34)
 (or (not v2) v52 (not v74))
 (or (not v27) (not v30) (not v5))
 (or (not v47) v70 v80)
 (or v79 (not v10) v70)
 (or v75 (not v84) (not v68))
 (or (not v28) (not v48) v43)
 (or (not v39) (not v9) v47)
 (or v1 v25 v74)
 (or v52 (not v81) v38)
 (or (not v73) (not v37) (not v33))
 (or (not v55) v7 v32)
 (or (not v52) v48 v2)
 (or v49 (not v16) (not v66))
 (or v40 v2 (not v13))
 (or (not v83) v37 (not v38))
 (or v39 (not v42) (not v45))
 (or v39 (not v69) (not v2))
 (or v46 v10 (not v4))
 (or v30 (not v64) (not v63))
 (or (not v71) v15 v64)
 (or (not v73) v53 (not v36))
 (or v8 v82 v45)
 (or v17 (not v2) v52)
 (or (not v62) (not v7) (not v47))
 (or v61 (not v55) v64)
 (or v33 (not v75) (not v82))
 (or v55 (not v64) (not v0))
 (or v82 (not v39) v55)
 (or v28 (not v60) v15)
 (or (not v82) v62 (not v32))
 (or (not v57) v3 (not v59))
 (or (not v5) (not v45) (not v11))
 (or (not v11) v44 v62)
 (or (not v47) (not v60) (not v41))
 (or (not v72) (not v45) v34)
 (or v29 (not v57) v74)
 (or (not v69) v42 v18)
 (or v11 (not v39) (not v46))
 (or v61 v28 (not v12))
 (or v59 (not v71) v63)
 (or v20 (not v54) (not v17))
 (or (not v57) (not v20) (not v3))
 (or (not v79) v71 (not v35))
 (or v80 v14 (not v60))
 (or (not v33) (not v26) (not v70))
 (or v9 (not v58) (not v73))
 (or (not v30) (not v81) (not v10))
 (or v25 (not v6) (not v16))
 (or (not v48) (not v49) (not v26))
 (or (not v7) (not v1) (not v59))
 (or v6 v16 v11)
 (or (not v62) (not v26) (not v80))
 (or (not v28) v55 (not v18))
 (or (not v12) v66 v80)
 (or v68 (not v69) v2)
 (or (not v75) v39 (not v45))
 (or (not v2) v57 v61)
 (or v39 (not v13) v57)
 (or (not v9) (not v49) (not v17))
 (or v60 (not v40) v63)
 (or (not v77) v51 v53)
 (or v50 (not v73) (not v26))
 (or v52 v16 v50)
 (or v72 v3 v42)
 (or v21 v83 (not v73))
 (or v49 v32 (not v3))
 (or v55 (not v61) (not v76))
 (or (not v40) v67 v42)
 (or (not v2) v59 v12)
 (or (not v21) (not v35) (not v3))
 (or (not v22) v2 (not v56))
 (or (not v25) v70 v36)
 (or v55 (not v44) (not v53))
 (or (not v75) (not v42) v62)
 (or v9 v31 v78)
 (or (not v58) (not v38) v55)
 (or (not v31) (not v66) (not v28))
 (or v72 (not v53) (not v15))
 (or (not v80) (not v11) v13)
 (or (not v69) (not v24) (not v39))
 (or (not v76) (not v5) (not v35))
 (or (not v52) v73 v8)
 (or v14 (not v35) (not v67))
 (or v65 (not v30) (not v50))
 (or (not v84) v37 v25)
 (or v63 v23 (not v12))
 (or (not v33) v7 (not v30))
 (or v74 (not v77) (not v22))
 (or (not v34) v40 v41)
 (or (not v13) v59 v65)
 (or (not v0) (not v10) v63)
 (or (not v60) (not v17) (not v42))
 (or v36 (not v63) v17)
 (or v72 (not v44) v73)
 (or (not v30) v26 v24)
 (or (not v12) (not v76) v79)
 (or v37 (not v40) (not v46))
 (or v50 v62 v53)
 (or (not v11) (not v23) (not v67))
 (or v3 (not v48) (not v37))
 (or v72 v37 v72)
 (or v11 v55 v6)
 (or (not v47) (not v16) (not v17))
 (or (not v16) (not v69) v27)
 (or (not v2) v49 (not v51))
 (or v59 v11 v64)
 (or (not v42) (not v24) (not v27))
 (or v75 (not v70) (not v24))
 (or v33 (not v13) v71)
 (or v65 v43 v0)
 (or v2 (not v49) (not v51))
 (or v6 (not v64) (not v37))
 (or (not v84) (not v17) (not v54))
 (or v34 v70 v22)
 (or v34 (not v27) v12)
 (or (not v48) v62 v55)
 (or v41 v11 (not v83))
 (or v63 v51 v3)
 (or (not v61) v59 v5)
 (or (not v44) v81 (not v71))
 (or (not v60) (not v17) v9)
 (or v32 v21 v72)
 (or (not v78) v50 v60)
 (or v44 (not v20) (not v82))
 (or v49 v18 (not v74))
 (or v63 v49 v51)
 (or (not v62) v64 v83)
 (or v41 (not v57) v27)
 (or (not v5) (not v67) (not v15))
 (or (not v61) (not v6) v13)
 (or v51 (not v55) v0)
 (or v1 v44 v28)
 (or (not v30) (not v26) v82)
 (or (not v52) (not v53) (not v41))
 (or (not v51) v66 (not v41))
 (or v15 v47 (not v62))
 (or (not v30) (not v66) v78)
 (or (not v15) v71 (not v36))
 (or (not v43) (not v75) v32)
 (or (not v27) (not v24) v36)
 (or v78 (not v27) (not v25))
 (or v20 (not v80) (not v34))
 (or (not v36) (not v67) (not v8))
 (or (not v62) v3 (not v24))
 (or (not v56) (not v11) v51)
 (or (not v2) (not v32) v35)
 (or (not v43) v74 v64)
 (or (not v45) (not v28) v68)
 (or v8 (not v7) (not v4))
 (or (not v74) v18 (not v11))
 (or v79 (not v63) v65)
 (or (not v20) v24 v15)
 (or v73 (not v33) v17)
 (or v61 v35 v72)
 (or (not v16) (not v21) (not v70))
 (or (not v4) v21 v22)
 (or (not v71) (not v4) v56)
 (or (not v30) (not v51) (not v6))
 (or v1 v76 (not v22))
 (or (not v31) (not v26) v33)
 (or (not v58) v39 v64)
 (or v0 (not v67) (not v66))
 (or v3 v10 v48)
 (or (not v34) v59 (not v13))
 (or v54 v72 (not v61))
 (or (not v45) (not v18) (not v55))
 (or v55 v80 (not v36))
 (or (not v6) v69 v78)
 (or v30 v8 (not v56))
 (or (not v2) (not v68) (not v79))
 (or (not v47) (not v54) v66)
 (or v41 v42 v33)
 (or (not v32) v36 v27)
 (or (not v62) (not v84) (not v42))
 (or v68 v55 v72)
 (or (not v34) (not v75) v38)
 (or (not v22) v35 v65)
 (or v27 (not v33) (not v23))
 (or v51 v19 v18)
 (or (not v4) (not v7) v34)
 (or v5 (not v4) (not v77))
 (or v17 v4 (not v42))
 (or v67 (not v22) (not v21))
 (or v53 (not v80) (not v83))
 (or (not v44) v39 v33)
 (or v1 v27 (not v43))
 (or v78 v70 v79)
 (or v81 (not v11) v53)
 (or (not v17) (not v49) (not v18))
 (or (not v6) v79 v49)
 (or v12 (not v7) v38)
 (or (not v36) (not v27) (not v71))
 (or (not v23) (not v31) v17)
 (or (not v65) (not v83) (not v45))
 (or v45 (not v65) v84)
 (or v69 (not v55) v84)
 (or (not v5) v52 (not v40))
 (or v16 (not v24) v74)
 (or v30 v20 v37)
 (or v15 (not v10) v0)
 (or (not v54) (not v40) (not v4))
 (or v12 v57 (not v28))
 (or v42 (not v80) (not v78))
 (or v80 v21 (not v41))
 (or v21 v13 (not v52))
 (or v43 (not v64) (not v6))
 (or (not v22) (not v24) (not v2))
 (or v24 (not v83) v20)
 (or (not v35) (not v58) (not v7))
 (or (not v15) v10 (not v51))
 (or v2 v24 v84)
 (or v82 (not v33) (not v2))
 (or (not v12) v52 (not v10))
 (or (not v51) (not v43) (not v68))
 (or v64 v29 (not v57))
 (or (not v66) (not v49) (not v5))
 (or (not v31) v49 (not v2))
 (or v38 v83 v53)
 (or v65 (not v18) v60)
 (or v81 v64 (not v35))
 (or (not v28) v53 v27)
 (or v24 v56 (not v74))
 (or (not v21) (not v38) v36)
 (or (not v7) (not v80) (not v71))
 (or (not v30) v32 (not v7))
 (or v73 v70 v33)
 (or v45 v41 (not v84))
 (or v42 (not v26) (not v14))
 (or v29 v9 v15)
 (or (not v19) v7 (not v73))
 (or v70 v18 v64)
 (or v11 (not v31) (not v14))
 (or (not v65) (not v52) v6)
 (or (not v9) v83 v24)
 (or v31 (not v28) v60)
 (or (not v83) v64 (not v33))
 (or v64 (not v75) (not v82))
 (or (not v17) (not v65) v73)
 (or (not v68) (not v33) v33)
 (or (not v65) v83 (not v71))
 (or v42 (not v56) (not v62))
 (or (not v16) (not v12) v58)
 (or v54 (not v45) v54)
 (or v12 v35 (not v21))
 (or v22 (not v55) v20)
 (or v45 v63 (not v51))
 (or v35 (not v16) (not v69))
 (or v14 v82 v6)
 (or (not v84) (not v32) (not v67))
 (or (not v37) v66 (not v27))
 (or v57 (not v6) (not v34))
 (or (not v82) (not v33) (not v27))
 (or v3 (not v12) v61)
 (or v29 v79 v20)
 (or (not v47) (not v55) (not v23))
 (or v4 v54 (not v45))
 (or v33 v68 v15)
 (or (not v67) (not v80) v15)
 (or (not v2) (not v25) (not v18))
 (or v15 (not v63) v23)
 (or v5 (not v51) v17)
 (or v71 v3 (not v40))
 (or (not v83) v67 (not v41))
 (or v53 (not v67) v31)
 (or (not v20) v11 (not v8))
 (or (not v83) (not v37) (not v51))
 (or (not v0) v83 v10)
 (or (not v60) (not v79) (not v32))
 (or v56 (not v62) v1)
 (or (not v62) (not v19) v33)
 (or (not v18) v33 v80)
 (or (not v73) v41 v55)
 (or (not v51) v46 v7)
 (or (not v25) v3 (not v59))
 (or (not v28) v69 (not v29))
 (or (not v51) (not v66) v38)
 (or (not v69) v43 v10)
 (or (not v58) (not v43) v6)
 (or v30 v35 v55)
 (or (not v20) v73 (not v84))
 (or (not v72) (not v52) (not v58))
 (or (not v34) v46 (not v4))
 (or v34 (not v26) v29)
 (or (not v5) (not v62) v51)
 (or (not v59) (not v12) (not v70))
 (or (not v84) v57 (not v69))
 (or v63 v39 v68)
 (or v60 (not v40) (not v24))
 (or (not v25) (not v58) v81)
 (or v20 v46 v30)
 (or (not v7) v47 v57)
 (or (not v25) (not v66) v9)
 (or (not v33) (not v26) v1)
 (or v31 v37 (not v71))
 (or v32 (not v50) v57)
 (or (not v41) (not v66) (not v66))
 (or (not v23) v54 v21)
 (or v47 v48 (not v71))
 (or (not v49) (not v52) (not v16))
 (or v3 (not v79) (not v39))
 (or (not v59) v80 v75)
 (or v57 (not v55) (not v78))
 (or v72 (not v74) v77)
 (or v2 (not v74) v3)
 (or (not v27) (not v66) v12)
 (or v8 (not v5) (not v77))
 (or (not v7) v84 (not v37))
 (or (not v70) (not v51) v63)
 (or v0 v15 (not v41))
 (or v48 v13 (not v48))
 (or (not v73) (not v28) (not v19))
 (or v81 v30 v12)
 (or (not v43) (not v9) (not v76))
 (or v34 v21 v3)
 (or v40 v80 v32)
 (or (not v78) (not v84) v55)
 (or (not v78) v47 v75)
 (or (not v5) v8 (not v0))
 (or (not v49) (not v19) (not v79))
 (or (not v32) v33 v70)
 (or (not v43) v46 v32)
 (or v30 (not v46) v12)
 (or (not v68) v83 v14)
 (or (not v52) v79 (not v77))
 (or (not v37) (not v0) v64)
 (or (not v26) (not v82) (not v34))
 (or (not v69) (not v54) v7)
 (or (not v59) v12 (not v61))
 (or v47 (not v53) v19)
 (or (not v39) v64 (not v12))
 (or v38 (not v29) v33)
 (or (not v2) v8 (not v32))
 (or v15 (not v60) v64)
 (or (not v81) v31 (not v12))
 (or (not v13) (not v52) (not v1))
 (or v26 v35 (not v31))
 (or (not v33) v21 (not v67))
 (or v64 (not v51) v67)
 (or (not v22) (not v76) v13)
 (or (not v62) (not v78) v57)
 (or v82 (not v64) v1)
 (or (not v75) v58 v7)
 (or (not v84) (not v47) v45)
 (or (not v19) v45 v44)
 (or v25 v51 (not v5))
 (or (not v60) (not v77) (not v13))
 (or v45 v71 v55)
 (or v51 v22 (not v33))
 (or v19 (not v80) v31)
 (or v56 v24 (not v51))
 (or (not v83) v57 (not v3))
 (or v76 (not v26) v69)
 (or v17 (not v80) v55)
 (or v6 (not v35) v52)
 (or (not v41) v12 v47)
 (or v16 v28 v44)
 (or v24 (not v29) v16)
 (or v13 v13 v67)
 (or v28 v75 (not v8))
 (or (not v12) (not v20) v31)
 (or (not v70) v69 (not v83))
 (or (not v4) (not v54) (not v0))
 (or (not v78) v67 (not v30))
 (or (not v41) (not v71) v38)
 (or v51 v64 v23)
 (or v31 v82 (not v27))
 (or v22 (not v67) v23)
 (or (not v40) v78 v7)
 (or (not v67) v59 (not v38))
 (or v11 (not v6) v40)
 (or v28 (not v68) v30)
 (or v12 (not v2) (not v65))
 (or v27 (not v31) v10)
 (or v70 v48 v8)
 (or v4 v83 (not v55))
 (or v58 v81 (not v81))
 (or (not v68) v48 (not v30))
 (or (not v53) (not v40) (not v3))
 (or v40 v65 v68)
 (or v55 v68 v8)
 (or v5 (not v55) v34)
 (or (not v15) v31 v28)
 (or v39 v15 v44)
 (or (not v14) v56 v24)
 (or v22 (not v39) v65)
 (or v20 v48 (not v47))
 (or v79 v66 v31)
 (or v24 v40 (not v78))
 (or (not v38) v72 (not v0))
 (or v9 v11 v9)
 (or v58 (not v56) (not v56))
 (or (not v40) (not v29) (not v38))
 (or v62 v24 v66)
 (or v68 (not v32) (not v30))
 (or v77 v13 v82)
 (or (not v57) (not v28) v71)
 (or v47 v41 (not v69))
 (or (not v7) (not v41) (not v23))
 (or v65 v52 v45)
 (or (not v37) v15 (not v41))
 (or (not v52) (not v16) v5)
 (or v32 (not v58) v7)
 (or v45 (not v7) (not v12))
 (or v4 (not v51) (not v47))
 (or (not v7) v78 (not v68))
 (or v65 v44 (not v22))
 (or (not v33) (not v59) (not v27))
 (or v27 v53 v16)
 (or v22 v61 (not v42))
 (or (not v32) (not v44) (not v58))
 (or (not v7) (not v37) (not v82))
 (or (not v11) (not v59) v51)
 (or (not v11) (not v16) v35)
 (or (not v54) (not v29) (not v67))
 (or (not v34) (not v29) (not v78))
 (or (not v45) v65 (not v75))
 (or v6 (not v83) (not v2))
 (or v84 v3 v64)
 (or v35 v0 (not v74))
 (or v47 v21 (not v52))
 (or v19 v38 (not v1))
 (or (not v17) (not v26) v8)
 (or (not v47) (not v84) v77)
 (or (not v48) v52 (not v62))
 (or (not v68) v45 (not v13))
 (or (not v4) (not v73) (not v10))
 (or v78 v10 v30)
 (or v61 v46 v14)
 (or v3 (not v23) v58)
 (or (not v81) v9 v58)
 (or (not v44) v32 (not v81))
 (or v1 (not v19) v40)
 (or v32 v33 (not v48))
 (or v27 v45 v1)
 (or (not v64) (not v80) v64)
 (or v27 (not v27) v71)
 (or (not v32) (not v12) v64)
 (or v24 v5 (not v40))
 (or (not v58) (not v60) v77)
 (or (not v46) (not v65) (not v70))
 (or v29 v6 v9)
 (or (not v54) (not v70) (not v34))
 (or v79 v29 v64)
 (or (not v1) v71 v70)
 (or (not v56) v55 v27)
 (or (not v43) v48 (not v64))
 (or (not v24) (not v33) v64)
 (or v0 (not v48) v6)
 (or v27 v37 v67)
 (or (not v27) (not v82) (not v58))
 (or (not v5) (not v70) (not v74))
 (or (not v59) v47 (not v36))
 (or v35 (not v52) (not v64))
 (or v23 (not v37) v49)
 (or (not v17) v62 (not v84))
 (or (not v7) (not v63) v76)
 (or v43 (not v36) v54)
 (or v83 (not v55) (not v5))
 (or (not v35) v54 v26)
 (or v33 v65 v1)
 (or v13 (not v27) v7)
 (or v60 v54 v37)
 (or (not v62) v75 (not v31))
 (or (not v14) v50 v61)
 (or v61 (not v13) (not v50))
 (or v68 v50 (not v39))
 (or (not v84) v32 (not v37))
 (or v16 (not v16) v40)
 (or v60 (not v63) (not v24))
 (or (not v5) (not v44) v74)
 (or v79 v44 v57)
 (or v51 (not v39) (not v57))
 (or v65 (not v23) v83)
 (or v54 (not v32) v9)
 (or (not v59) v80 (not v43))
 (or v39 v31 v17)
 (or (not v43) v75 (not v35))
 (or (not v67) (not v66) v68)
 (or v58 v50 (not v70))
 (or v33 v25 (not v12))
 (or (not v8) (not v75) v64)
 (or (not v9) (not v56) v4)
 (or (not v20) v56 (not v8))
 (or (not v76) (not v47) (not v53))
 (or (not v34) v24 (not v74))
 (or v71 (not v46) v78)
 (or (not v44) (not v17) v28)
 (or v23 (not v8) v68)
 (or (not v38) (not v40) (not v84))
 (or v61 (not v84) v47)
 (or v9 v52 (not v74))
 (or v32 (not v81) (not v63))
 (or v14 (not v70) (not v13))
 (or v0 (not v37) (not v53))
 (or (not v81) (not v56) (not v83))
 (or v51 v68 v1)
 (or (not v76) v50 v55)
 (or v31 v11 (not v78))
 (or (not v80) (not v46) v10)
 (or (not v66) v0 (not v36))
 (or (not v74) v53 (not v31))
 (or v61 (not v77) v10)
 (or v42 v17 v82)
 (or v26 v59 v38)
 (or (not v29) v74 v10)
 (or v48 v16 (not v45))
 (or v76 (not v70) (not v80))
 (or v41 v78 v43)
 (or v59 v13 (not v66))
 (or v46 v74 v37)
 (or v60 (not v81) v74)
 (or v71 v80 v57)
 (or v28 (not v79) (not v42))
 (or v35 v24 (not v9))
 (or v50 v12 (not v17))
 (or v61 v83 v83)
 (or v58 v17 v42)
 (or v66 v56 v24)
 (or (not v33) v4 (not v63))
 (or v18 v13 v9)
 (or (not v18) (not v42) (not v65))
 (or v47 (not v81) v17)
 (or (not v4) v79 v51)
 (or v73 v71 (not v72))
 (or v81 (not v78) (not v9))
 (or v33 v52 (not v10))
 (or (not v40) v15 v80)
 (or v49 (not v36) (not v63))
 (or (not v21) v77 (not v11))
 (or (not v25) (not v79) (not v4))
 (or v65 v47 v84)
 (or v68 (not v71) v19)
 (or v37 v21 (not v17))
 (or v39 v11 v55)
 (or (not v75) v16 v27)
 (or v65 v27 v66)
 (or v70 (not v73) v26)
 (or v66 (not v2) v65)
 (or (not v77) v13 v24)
 (or v75 (not v66) v3)
 (or v66 v43 (not v40))
 (or (not v24) v53 (not v40))
 (or v30 v22 (not v52))
 (or v13 (not v15) (not v65))
 (or v17 v52 (not v80))
 (or (not v73) v11 (not v5))
 (or v15 (not v24) v75)
 (or v72 (not v18) (not v53))
 (or (not v8) v48 v33)
 (or (not v82) v49 (not v64))
 (or (not v42) v6 (not v38))
 (or v33 v36 (not v27))
 (or v68 (not v59) (not v18))
 (or (not v62) (not v22) (not v27))
 (or v58 v73 v83)
 (or (not v79) (not v51) (not v38))
 (or v23 v18 v41)
 (or (not v13) (not v20) v32)
 (or (not v84) (not v71) v74)
 (or (not v77) v67 v48)
 (or v83 v20 v20)
 (or (not v45) v35 (not v73))
 (or v77 (not v50) (not v83))
 (or (not v66) (not v20) (not v71))
 (or v1 v59 (not v1))
 (or v7 v7 v61)
 (or v81 (not v50) v71)
 (or v30 v63 (not v62))
 (or v16 (not v63) v81)
 (or (not v43) v41 (not v19))
 (or (not v36) v3 v51)
 (or v62 (not v77) (not v56))
 (or (not v2) v21 v57)
 (or v20 (not v65) (not v71))
 (or v52 v51 (not v53))
 (or v51 v6 (not v23))
 (or (not v29) v48 v21)
 (or (not v48) (not v53) v57)
 (or v72 (not v49) (not v21))
 (or v57 (not v69) v32)
 (or v10 (not v52) v49)
 (or (not v66) (not v28) (not v32))
 (or v80 (not v37) v75)
 (or v19 (not v47) v12)
 (or (not v20) v48 (not v48))
 (or v41 (not v13) (not v29))
 (or v16 (not v76) v19)
 (or (not v36) v29 (not v75))
 (or (not v84) v82 v18)
 (or v44 (not v70) (not v59))
 (or (not v69) v29 (not v54))
 (or (not v40) (not v20) v44)
 (or (not v67) v63 v60)
 (or v3 (not v12) (not v72))
 (or (not v3) v39 (not v46))
 (or (not v10) v54 (not v70))
 (or v30 (not v62) (not v38))
 (or (not v80) (not v15) (not v30))
 (or v47 (not v22) v46)
 (or (not v58) v59 v52)
 (or v26 (not v30) (not v28))
 (or v76 v83 (not v77))
 (or (not v69) (not v20) (not v53))
 (or v10 (not v69) (not v22))
 (or (not v14) v45 (not v8))
 (or (not v39) (not v79) (not v61))
 (or v48 v15 (not v13))
 (or (not v43) v20 v24)
 (or v81 (not v51) (not v37))
 (or (not v72) v68 (not v64))
 (or v2 (not v79) (not v47))
 (or (not v26) (not v73) v73)
 (or v84 v6 v16)
 (or (not v31) (not v13) (not v1))
 (or v65 v16 v7)
 (or (not v67) (not v6) v65)
 (or (not v58) v18 (not v64))
 (or v47 (not v34) v48)
 (or (not v66) v73 (not v54))
 (or v59 (not v72) v44)
 (or v53 (not v68) v34)
 (or v54 (not v18) v28)
 (or (not v67) v5 v12)
 (or (not v77) (not v56) (not v41))
 (or (not v0) v55 (not v44))
 (or v79 v16 (not v36))
 (or (not v63) v77 (not v32))
 (or v83 (not v47) (not v42))
 (or v39 v11 v1)
 (or (not v21) v58 v62)
 (or (not v79) (not v67) (not v5))
 (or (not v28) (not v17) (not v13))
 (or (not v34) v49 v13)
 (or v30 (not v48) v57)
 (or v64 (not v67) v38)
 (or (not v19) v32 v42)
 (or (not v64) v7 (not v77))
 (or v33 v83 (not v58))
 (or (not v69) v1 v20)
 (or (not v23) (not v30) (not v8))
 (or v24 v17 v44)
 (or (not v77) (not v9) v54)
 (or (not v74) v43 (not v73))
 (or (not v79) (not v15) (not v3))
 (or v4 v81 v77)
 (or (not v41) (not v65) v14)
 (or v74 (not v62) (not v55))
 (or (not v60) (not v63) v83)
 (or (not v36) v0 (not v81))
 (or v41 (not v5) v65)
 (or (not v22) (not v42) (not v52))
 (or (not v48) (not v70) (not v44))
 (or v24 v19 (not v67))
 (or v54 (not v28) (not v82))
 (or (not v61) (not v50) (not v26))
 (or v82 v0 v7)
 (or (not v77) v52 (not v27))
 (or (not v4) (not v34) (not v66))
 (or v13 v79 (not v3))
 (or (not v7) (not v76) (not v26))
 (or (not v80) (not v37) (not v69))
 (or (not v56) v35 v27)
 (or v48 v37 (not v11))
 (or v44 (not v1) (not v6))
 (or v40 (not v45) (not v12))
 (or (not v31) v58 v63)
 (or v73 v84 v3)
 (or (not v82) v38 (not v48))
 (or (not v12) (not v47) v73)
 (or v14 v59 (not v2))
 (or (not v21) (not v46) v20)
 (or v19 (not v44) v80)
 (or v43 v24 v38)
 (or (not v59) v4 (not v39))
 (or v70 v79 (not v44))
 (or (not v1) (not v84) v51)
 (or v20 v65 (not v2))
 (or (not v45) v0 (not v49))
 (or v67 (not v5) (not v72))
 (or (not v7) v84 v14)
 (or v11 (not v51) (not v83))
 (or v71 v6 (not v62))
 (or v52 (not v73) (not v15))
 (or v37 (not v44) (not v81))
 (or (not v84) v4 (not v64))
 (or v77 v31 v10)
 (or (not v3) v27 (not v16))
 (or v33 v81 (not v31))
 (or (not v49) (not v5) v39)
 (or v75 v0 v10)
 (or v75 (not v75) (not v26))
 (or v81 v81 (not v23))
 (or (not v26) (not v11) v56)
 (or (not v34) (not v33) (not v1))
 (or v78 (not v68) v54)
 (or (not v13) (not v32) v45)
 (or (not v5) (not v81) v27)
 (or (not v52) (not v18) (not v56))
 (or v48 (not v19) (not v58))
 (or v22 (not v74) (not v16))
 (or v58 (not v39) v3)
 (or (not v80) (not v78) (not v53))
 (or v67 v9 (not v23))
 (or (not v79) v4 (not v59))
 (or v78 v0 (not v82))
 (or (not v39) v69 v23)
 (or v3 (not v26) v11)
 (or v39 (not v31) v65)
 (or (not v15) v5 v14)
 (or v45 (not v37) (not v23))
 (or (not v66) (not v4) v38)
 (or v8 (not v6) (not v64))
 (or (not v51) v39 v54)
 (or (not v70) (not v74) (not v7))
 (or v30 v51 v69)
 (or v43 (not v12) v29)
 (or (not v29) v55 v82)
 (or v66 (not v63) (not v27))
 (or (not v83) (not v29) (not v15))
 (or (not v6) (not v70) (not v79))
 (or (not v7) (not v59) v53)
 (or (not v36) v8 (not v21))
 (or v35 (not v43) (not v53))
 (or v75 v70 (not v52))
 (or (not v52) (not v49) (not v54))
 (or v14 (not v70) (not v6))
 (or (not v84) (not v40) (not v27))
 (or (not v20) (not v20) v84)
 (or (not v75) (not v55) v66)
 (or v44 v83 v9)
 (or (not v41) (not v18) v22)
 (or (not v75) (not v36) (not v8))
 (or v31 (not v28) (not v55))
 (or (not v0) v76 v50)
 (or v74 (not v63) (not v43))
 (or (not v63) v2 (not v80))
 (or v6 v19 v24)
 (or (not v69) (not v13) (not v51))
 (or (not v51) (not v18) (not v61))
 (or (not v49) v54 (not v35))
 (or v73 v74 (not v6))
 (or v42 v21 (not v78))
 (or (not v79) v76 v42)
 (or v64 (not v63) (not v76))
 (or (not v71) (not v46) (not v73))
 (or v17 v22 (not v50))
 (or (not v20) (not v14) v18)
 (or v44 (not v17) v79)
 (or (not v8) v53 (not v19))
 (or v11 v2 v64)
 (or (not v47) v18 (not v68))
 (or (not v9) (not v79) (not v34))
 (or (not v39) v16 v7)
 (or (not v64) v47 (not v2))
 (or (not v25) v26 v17)
 (or (not v34) v20 v31)
 (or (not v44) v79 v78)
 (or (not v32) v37 (not v79))
 (or (not v65) (not v3) (not v44))
 (or v11 (not v63) v33)
 (or v69 v15 (not v70))
 (or v59 (not v4) (not v48))
 (or v51 v9 v35)
 (or (not v5) v47 v24)
 (or v27 (not v33) v2)
 (or v24 (not v15) v25)
 (or v34 v35 v19)
 (or (not v74) v37 (not v70))
 (or (not v64) v47 (not v60))
 (or v84 (not v64) v31)
 (or v25 v45 (not v39))
 (or v36 (not v9) (not v54))
 (or v5 v47 v3)
 (or (not v14) v1 (not v14))
 (or (not v41) v11 v33)
 (or v59 (not v56) (not v14))
 (or (not v82) (not v3) v24)
 (or (not v57) v15 v22)
 (or v82 v68 v75)
 (or v27 (not v62) v0)
 (or (not v5) (not v75) (not v25))
 (or v24 v58 (not v63))
 (or (not v78) v8 v26)
 (or v23 (not v15) v68)
 (or v18 v79 (not v55))
 (or v16 v21 v63)
 (or (not v64) (not v28) (not v10))
 (or v46 (not v59) (not v73))
 (or (not v52) (not v77) v47)
 (or v31 v17 (not v34))
 (or v7 (not v36) v62)
 (or v63 v58 v14)
 (or (not v70) (not v0) (not v78))
 (or v50 v44 v36)
 (or (not v28) (not v43) v53)
 (or (not v2) (not v1) (not v63))
 (or (not v13) v34 (not v25))
 (or (not v64) (not v28) v30)
 (or (not v6) v54 (not v83))
 (or (not v20) v34 (not v32))
 (or (not v74) (not v55) v5)
 (or (not v63) v28 v56)
 (or (not v47) v10 (not v11))
 (or v8 v55 v5)
 (or (not v60) (not v80) v47)
 (or (not v12) v77 (not v57))
 (or v14 (not v37) v80)
)))
e85
))

(check-sat)
